Nuprl Definition : f-rank 11,40

f-rank{i:l}
f-rank(xfreeese)
== if x changed before e
== then let r = f-rank{i:l}
== then let r = f-rank(xfreees; (last change to x before e)) in
== then let rif eq_id(es-after(esxe); free) then inc-fst(r) else inc-snd(r) fi 
== else <0, 1>
== fi 


clarification:

f-rank{i:l}
f-rank(xfreeese)
== if changed{i:l}
== if changed(Id; id-deq; esxe)
== then let r = f-rank{i:l}
== then let r = f-rank(xfreees; last-change{i:l}(Id; id-deq; esxe)) in
== then let rif eq_id(es-after(esxe); free) then inc-fst(r) else inc-snd(r) fi 
== else <0, 1>
== fi 
(recursive) 
latex


DefinitionsY, x.A(x), x changed before e, let x = a in b(x), f(a), (last change to x before e), Id, id-deq, if b then t else f fi , eq_id(ab), es-after(esxe), inc-fst(p), inc-snd(p), <ab>, #$n
FDL editor aliasesf-rank

origin